/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.bool;

import java.io.File;
import java.util.ArrayList;
import java.util.Collection;
import java.util.Collections;
import java.util.List;

import alloy.util.Dbg;
import alloy.util.ObjID;
import alloy.util.Util;

/**
 * BooleanFormula, represents an arbitrary boolean formula.
 * The only publicly visible representation of Boolean formulas.
 * {@link BooleanFormula}s are immutable (although right now some
 * {@linkplain BoolTemplateInstance annotations} may be {@linkplain #recordCachingInfo written} onto the BooleanFormula objects).
 * <p>
 * The #equals method is guaranteed to correctly detect the equivalence of
 * Boolean literals (created by {@link #makeLit}); i.e.,
 * the {@link BooleanFormula}s returned by all calls to {@link #makeLit}(1)
 * are guaranteed to be {@link #equal}.  Also, {@link #TRUE} and {@link #FALSE}
 * are guaranteed to be the only {@link BooleanFormula}s representing these
 * constants, so testing for equality to them can be done using <code>==</code>.
 */
public abstract class BooleanFormula extends ObjID {
	/** 
	 * These "singletons" have mutable state, and hence need to be initialized for each compilation.
	 * These fields should only be set by the initSingletons() method below.
	 */
    private static /*final*/BooleanFormula FALSE = null; //new GBF_Const(false);
    private static /*final*/ BooleanFormula TRUE = null; //new GBF_Const(true);

    public static BooleanFormula TRUE() { return TRUE; }
	public static BooleanFormula FALSE() { return FALSE; }

    /**
     * Should be called before each compile.
     *
     */
    public static void initSingletons() {
        FALSE = new GBF_Const(false);
        TRUE = new GBF_Const(true);
        GBF_Lit.initSingletons();
        Eval_V.initSingleton();
        BLBackend.initSingleton();
        BoolSimplifyVisitor.initSingleton();
        PartialAssignment.initSingleton();
        UcoreProofProcessor.initSingleton();
    }
    
    /**
     * An informational number written on a Boolean node that identifies
     * where the node came from (e.g. from which Alloy AST node this
     * Boolean node was translated).
     */
    private int _nodeSrc;

    /** The node source given to newly created nodes */
    private final static int _sDefaultNodeSrc = 0;


	public static void setDefaultNodeSrc(int defaultNodeSrc_) {
    //_sDefaultNodeSrc = defaultNodeSrc_;
    }

    public void setNodeSrc(int nodeSrc_) { _nodeSrc = nodeSrc_; }
    public int getNodeSrc() { return _nodeSrc; }

    public static BooleanFormula makeConst(boolean val_) { return val_ ? TRUE() : FALSE(); }
    /** @return true iff the formula is a Boolean constant ({@link #TRUE} or {@link #FALSE}). */
    public boolean isConst() { return this instanceof GBF_Const; }

    // for caching the value computed by isConstantValued()
    
    private static final int UNCOMPUTED = 0;
    private static final int CONSTANT_VAL = 1;
    private static final int NOT_CONSTANT = 2;

    private int cachedConstVal = UNCOMPUTED;
    /**
     * @return true iff the formula is constant-valued, i.e. if its value is completely
     *         determined at grounding-out time.  This happens iff its leaves are only
     *         {@link #makeConst constants} or {@link #makeSwitchableConst switchable constants},
     *         and not {@link #makeLit literals}.
     */
    public final boolean isConstantValued() {
        if (cachedConstVal == UNCOMPUTED) {
            if (checkConstantValued()) {
                cachedConstVal = CONSTANT_VAL;
            } else {
                cachedConstVal = NOT_CONSTANT;
            }
        }
        return cachedConstVal == CONSTANT_VAL;
    }

    protected abstract boolean checkConstantValued();
    
    public static BooleanFormula makeLit(int var) { return GBF_Lit.getLitObj(var); }

    public boolean isLiteral() { return this instanceof GBF_Lit; }
    public int getLiteral() { return ((GBF_Lit)this).getLit(); }
    public boolean isSwitchableConst() { return this instanceof VarConst; }

    /** Create a {@link BooleanFormula} whose interpretation is either
    constant {@link #TRUE} or constant {@link #FALSE} depending on
    the current value of a given {@link BoolSwitch}.  The interpretation
    is TRUE iff bit number testBit_ is set in the current value of
    the {@link BoolSwitch}, and false otherwise. */
    public static BooleanFormula makeSwitchableConst(BoolSwitch var_, long val_) {
    BooleanFormula result = new VarConst(var_, val_);
    result.setNodeSrc(_sDefaultNodeSrc);
    return result;
    }

    /**
     * Simplify this boolean formula using the given partial assignment.
     * Return a reference to the simplified version of the boolean formula
     * (recall that {@link BooleanFormula}s are immutable).
     */
    public BooleanFormula simplify(PartialAssignment pa_) {
    return (BooleanFormula)acceptVisitor(new BoolSimplifyVisitor(pa_));
    }

    /** Create a {@link BooleanFormula} whose interpretation is
    "set this {@link BoolSwitch} to this value and interpret
    this {@link BooleanFormula} (presumably containing some
    {@link #makeSwitchableConst switchable constants} that
    depend on this switch). */
    public static BooleanFormula makeSwitch(BoolSwitch var_, long val_,
                        BooleanFormula f_) {
    BooleanFormula result = new SetVarExpr(var_, val_, f_);
    result.setNodeSrc(_sDefaultNodeSrc);
    return result;
    }

    public String dbg() { return toString(); }
    /*------------------------------------------------------------*/

    public BooleanFormula and(BooleanFormula f) {
    if (this == TRUE()) return f;
    if (this == FALSE()) return this;
    if (f == TRUE()) return this;
    if (f == FALSE()) return FALSE();
    if (this instanceof GBF_Lit && f instanceof GBF_Lit) {
        GBF_Lit g1 = (GBF_Lit)this;
        GBF_Lit g2 = (GBF_Lit)f;
        if (g1 == g2.opposite()) return FALSE();
    }
    BooleanFormula result = new GBF_And(this,f);
    result.setNodeSrc(_sDefaultNodeSrc);
    return result;
    }

    public BooleanFormula or(BooleanFormula f) {
    if (this == TRUE()) return this;
    if (this == FALSE()) return f;
    if (f == FALSE()) return this;
    if (f == TRUE()) return TRUE();
        BooleanFormula result = new GBF_Or(this,f);
    result.setNodeSrc(_sDefaultNodeSrc);
    return result;
    }

    public static BooleanFormula makeOr(BooleanFormula[] formulas_) {
    if (formulas_.length == 0) return FALSE();
    if (formulas_.length == 1) return formulas_[0];

    if (false)
        return new GBF_Or(formulas_);
    else {
        int newChildCount = 0;
        for (int i=0; i<formulas_.length; i++) {
        if (formulas_[i] == TRUE()) return TRUE();
        if (formulas_[i] != FALSE())
            newChildCount++;
        }
        if (newChildCount == formulas_.length)
	    return new GBF_Or(formulas_);
        if (newChildCount == 0)
	    return FALSE();

        BooleanFormula[] newChildren = new BooleanFormula[newChildCount];
        int newChildLen = 0;
        for (int i=0; i<formulas_.length; i++)
        if (formulas_[i] != FALSE())
            newChildren[newChildLen++] = formulas_[i];
        if (newChildren.length == 1)
        return newChildren[0];
        return new GBF_Or(newChildren);
    }
    //return _makeOr(formulas_, 0, formulas_.length);
    }

    private static BooleanFormula _makeOr(BooleanFormula[] formulas_, int from_, int to_) {
        if (from_ >= to_) return FALSE();
        if (from_+1 == to_) return formulas_[from_];
        int mid = (from_ + to_) / 2;
        return _makeOr(formulas_, from_, mid).or(_makeOr(formulas_, mid, to_));
    }

    public static BooleanFormula makeAnd(BooleanFormula[] formulas_) {
        if (formulas_.length == 0) return TRUE();
        if (formulas_.length == 1) return formulas_[0];

        if (false)
            return new GBF_And(formulas_);
        else {
            int newChildCount = 0;
            for (int i=0; i<formulas_.length; i++) {
            if (formulas_[i] == FALSE()) return FALSE();
            if (formulas_[i] != TRUE())
                newChildCount++;
            }
            if (newChildCount == formulas_.length)
            return new GBF_And(formulas_);
            if (newChildCount == 0)
            return TRUE();

            BooleanFormula[] newChildren = new BooleanFormula[newChildCount];
            int newChildLen = 0;
            for (int i=0; i<formulas_.length; i++)
            if (formulas_[i] != TRUE())
                newChildren[newChildLen++] = formulas_[i];
            if (newChildren.length == 1)
            return newChildren[0];
            return new GBF_And(newChildren);
        }
        //return _makeAnd(formulas_, 0, formulas_.length);
    }

    private static BooleanFormula _makeAnd(BooleanFormula[] formulas_, int from_, int to_) {
        if (from_ >= to_) return TRUE();
        if (from_+1 == to_) return formulas_[from_];
        int mid = (from_ + to_) / 2;
        return _makeAnd(formulas_, from_, mid).and(_makeAnd(formulas_, mid, to_));
    }

    public static BooleanFormula makeOr(Collection/*<of BooleanFormula>*/ formulas_) {
        return makeOr((BooleanFormula[])formulas_.toArray(new BooleanFormula[]{}));
    }

    public static BooleanFormula makeAnd(Collection/*<BooleanFormula>*/ formulas_) {
        return makeAnd((BooleanFormula[])formulas_.toArray(new BooleanFormula[]{}));
    }

    public BooleanFormula not() {
        if (this == TRUE()) return FALSE();
        if (this == FALSE()) return TRUE();
        // check if it's a unit clause -- if yes, negate without a GBF_Not
        if (this instanceof GBF_Lit) return ((GBF_Lit)this).opposite();
        // check if it's a negation -- if yes, return the negated formula
        if (this instanceof GBF_Not) return ((GBF_Not)this).getExpr();
        // otherwise just insert a GBF_Not node
        BooleanFormula result =  new GBF_Not(this);
        result.setNodeSrc(_sDefaultNodeSrc);
        return result;
    }

    public BooleanFormula implies(BooleanFormula f) {
        return (this.not()).or(f);
    }

    public BooleanFormula bool_equals(BooleanFormula f) {
        return this.implies(f).and(f.implies(this));
    }

    public BooleanFormula iff(BooleanFormula f) { return bool_equals(f); }

    public static BooleanFormula makeCNFFunc(BooleanFormula[] children_, List /* of int[] */ clauses_) {
        return new CNFFunc(children_, clauses_);
    }

    /** Evaluate this boolean formula with respect to the given complete assignment
    to all Boolean variables used in the formula.
    @param assignment_ values of boolean vars; assignment_[0] unused, assignment_[i]
    gives value of var i */
    public boolean interpret(boolean[] assignment_) {
        if (assignment_ == null) return interpret();
        return acceptVisitor(new Eval_V(assignment_)) == TRUE();
    }

    public boolean interpret(PartialAssignment pa_) {
      return interpret(pa_.toBoolArray());
    }

    /** Return the current value of a constant-valued formula. */
    public boolean interpret() {
      return acceptVisitor(Eval_V.sDefaultEval_V) == TRUE();
    }

    // stats & size are currently stubs
    public String stats() { return "stats"; }
    public int size() { return 1; }

    public void setNegation(BooleanFormula f) {
    // negation caching is implemented here by the use of GBF_Not nodes
    }

    public void dump() {
        WriteSAT_V wsv = new WriteSAT_V(System.err);
        acceptVisitor(wsv);
        wsv.flush();
    }

    public void dump(String msg) { System.err.println(msg); dump(); }

    /** Write the formula to a .sat file for solving with a
    SAT solver.  May take a while for large formulas.
    @param fileName_ name of target .sat file (will be overwritten)
    @param nvars_ upper bound on the number of boolean variables used in the formula
    @param dependentVars_ for each boolean variable, whether it is dependent,
    i.e. whether its value is uniquely determined by the values of independent
    variables.  solving may work faster in some cases if dependent variables
    are explicitly identified in this way: the actual search space is
    2^{# of <em>independent</em>} variables. */
    public void writeSatFile (File fileHandle_,
                  int nvars_,
                  boolean[] dependentVars_) {
    Dbg.info("Dumping formula to file: " + fileHandle_+"...");
    WriteSAT_V wsv = new WriteSAT_V(fileHandle_, nvars_, dependentVars_);
    acceptVisitor(wsv);
    wsv.close();
    //wsv.printFreqs();
    Dbg.info("Dumped formula to " + fileHandle_);
    }

    public void writeSatFile(File fileHandle_, int nvars_)
    { writeSatFile(fileHandle_, nvars_, null /* dependentVars_ */ ); }

    public static final int MULT_SET = 0;
    public static final int MULT_SCALAR = 1;
    public static final int MULT_OPTION = 2;

    /**
     * Record caching information for this {@link BooleanFormula},
     * to be used during grounding-out to avoid grounding-out this
     * BooleanFormula node in some cases.
     * <p>
     * This method may be called multiple times to record
     * caching information, which accumulates.  Note that this
     * is the only method that mutates the BooleanFormula object.
     */
    public void recordCachingInfo(int templCacheId_,
                  BooleanFormula[] templCacheKey_,
                  int[] templArgScopes_,
                  int[] templArgMults_) {
	// if the cache key would be >63 bits long -- ignore the caching info, for now.
	int keyLen = 0;
	for (int i=0; i<templArgScopes_.length; i++) {
	    if (templArgMults_[i] == MULT_SET)
		keyLen += templArgScopes_[i];
	    else if (templArgMults_[i] == MULT_SCALAR)
		keyLen += Util.binaryLogUp(templArgScopes_[i]);
	    else if (templArgMults_[i] == MULT_OPTION)
		keyLen += Util.binaryLogUp(templArgScopes_[i] + 1);
	    else Dbg.fatal("unknown multiplicity");
	}
	if (keyLen > 64)
	    return;

	for (int i=0; i<templCacheKey_.length; i++) {
	    if (!templCacheKey_[i].isConstantValued())
		return;
	}
	
        final BoolTemplateInstance inst = new BoolTemplateInstance(
        		templCacheId_,
        		templCacheKey_,
        		templArgScopes_,
        		templArgMults_);
        //boolTemplInsts.clear();
        
        if (boolTemplInsts==null) {
        	boolTemplInsts = new ArrayList();
        }
        //boolTemplInsts.clear();
        getBoolTemplInsts().add(inst);
    }

    List /* of BoolTemplateInstance */ getBoolTemplInsts() {
		return boolTemplInsts==null ? Collections.EMPTY_LIST : boolTemplInsts;
	}

    /**
     * This will be instantiated, if necessary, by recordCachingInfo.
     * getBoolTemplInsts() is the accessor both internally and externally.
     */
	private List /* of BoolTemplateInstance */ boolTemplInsts = null;// new ArrayList();

    public void printTemplateInfo() {
        System.out.println(getBoolTemplInsts());
    }

    private String _descr;
    public String getDescr() { return _descr; }
    public void setDescr(String descr_) { _descr = descr_; }

    /** Last visitor to have visited this node.  Used by visitors to check
    whether they have already visited this node.  */
    GBF_V lastVisitor = null;

    /** The value returned by the last visitor to visit this node. */
    Object lastVisitorResult;

    /** Node ID of this node when writing to a .sat file; set by {@link WriteSAT_V} during traversal. */
    long satFileNodeId;

    Object acceptVisitor(GBF_V visitor_) {
    Object result = handleVisitor(visitor_);
    // critical: we don't want to change lastVisitor to visitor_
    // until we have called handleVisitor().  otherwise, the visitor
    // will think it has already visited this node before, whereas in fact
    // this is a first-time visit.
    lastVisitor = visitor_;
    lastVisitorResult = result;
    return result;
    }

    /** Overridden by specific nodes to implement visitor behavior
    i.e. call forXXXX method of visitor_ for the node type. */
    protected abstract Object handleVisitor(GBF_V visitor_);

    /**
     * Returns the index of the highest variable used by
     * this expression.
     */
    abstract int getNumVars();

    /**
     * Take an array of Boolean formulas (which may share subformulas),
     * and write a BLIF file defining a circuit whose inputs are the Boolean
     * variables used in the formulas, and whose outputs are the formulas.
     */
    public static void writeBLIF(String fname_, int nvars_, BooleanFormula[] bformulas_) {
    WriteBLIF_V blifVisitor = new WriteBLIF_V(fname_, nvars_, bformulas_);
    for (int i=0; i<bformulas_.length; i++)
        bformulas_[i].acceptVisitor(blifVisitor);
    blifVisitor.close();
    }

}  // classs BooleanFormula


